#include "dpll_pthread.h"
#include "timer.h"
#include "dpll.h"
#include<pthread.h>
#include"sse_avx.h"
#include<stdlib.h>
extern timer tm;
int CERR_LEVELS[THREADNUM] = {0}; 
_bool stop;
extern long long threshold;
static dpllresult* DPLLalgorithm_pth(cnf* cnf);
pthread_mutex_t oricnf_m;
_bool dpll_satisfiable_pth(cnf*_cnf){
    printf("start \n");
    dpllresult* result = DPLLalgorithm_pth(_cnf);
    if (result == NULL) return false;
    if (result->model_cnf != NULL){
        _cnf = new_cnf_from(result->model_cnf);
        print_cnf(_cnf);
    }
    return result->sat;
}
void print_vars(variable* vars, int n);
dpll_task_t* new_task(variable* var_set, int n_univar){
    dpll_task_t* task = (dpll_task_t*)malloc(sizeof(dpll_task_t));
    task->n_univar = n_univar;
    int var_set_size = n_align(sizeof(variable) * n_univar, _ALIGN_);
    task->vars_set = (variable*)malloc(var_set_size);
    for(int i = 0; i < task->n_univar; i++){
        task->vars_set[i].name = var_set[i].name;
        task->vars_set[i].value = var_set[i].value;
        task->vars_set[i].assigned = var_set[i].assigned;
    }
    //print_vars(task->vars_set, task->n_univar);
    return task;
}

void free_task(dpll_task_t* task){
    if(task == NULL) return;
    free(task->vars_set);
    free(task); 
}
/**
 * tasklist_mutex => mutex for visiting tasklist, 
 *                  this is not very time consuming
 * path_mutex     => mutex for copying var_set when 
 *                  allocating job for a thread  
 * continue_mutex => mutex for stopper
 */
pthread_mutex_t stop_state_mutex, continue_mutex, path_mutex[THREADNUM], tasklist_mutex;
pthread_cond_t cond;
pthread_t thread[THREADNUM];
pthread_param_t params[THREADNUM];

cnf* thread_cnf[THREADNUM];
static int numtask;
list_entry_t task_list;
_bool stop_state[THREADNUM];
static void init_all_mutex(){
    pthread_mutex_init(&continue_mutex, NULL);
    pthread_mutex_init(&oricnf_m, NULL);
    pthread_mutex_init(&stop_state_mutex, NULL);
    pthread_cond_init(&cond, NULL);
    for(int i = 0; i < THREADNUM; i++){
        stop_state[i] = true;
        pthread_mutex_init(&path_mutex[i], NULL);
    }
}

static void destroy_all_mutex(){
    pthread_mutex_destroy(&continue_mutex);
    pthread_mutex_destroy(&oricnf_m);
    pthread_mutex_destroy(&stop_state_mutex);
    for(int i = 0; i < THREADNUM; i++){
        pthread_mutex_destroy(&path_mutex[i]);
    }
}



static void task_reload(cnf* cnf, dpll_task_t* task, int threadid);
static dpllresult* DPLLalgorithm2(cnf* cnf, int threadid);
static dpllresult* DPLLalgo_thread(void* params){
    //load thread params
    pthread_param_t* taskparams = (pthread_param_t*) params;
    int threadid = taskparams->threadID;


    while (true){
        //stop check, triggered when other thread founds a solution
        pthread_mutex_lock(&continue_mutex);
        if (stop) {
            pthread_mutex_unlock(&continue_mutex);
            printf("[thread %d]stopped by mark\n", threadid);
            break;
        }
        pthread_mutex_unlock(&continue_mutex);

        //assign task for the thread
        dpll_task_t* task = NULL;
        pthread_mutex_lock(&tasklist_mutex);
        //printf("[thread %d] checking task list\n", threadid);
        while(numtask == 0){
            pthread_cond_wait(&cond, &tasklist_mutex);
            //check if all fail (fail in all paths, and no path left in task list)
            pthread_mutex_lock(&stop_state_mutex);
            _bool dead = true;
            for(int i = 0; i < THREADNUM; i++){
                if (!stop_state[i]) dead = false;
            }
            if (dead) {
                printf("[thread %d]killed by dead flag\n", threadid);

                pthread_mutex_unlock(&stop_state_mutex);
                pthread_mutex_unlock(&tasklist_mutex);
                //try stop others
                pthread_cond_signal(&cond);
                
                return NULL;
            }
            pthread_mutex_unlock(&stop_state_mutex);
        }
        while (true){
            if (numtask > 0){
                task = le2task(list_prev(&task_list), entry);
                list_del(&task->entry); //deletefrom list
                numtask--;        
                //printf("[thread %d] took away a task ,now %d left\n ", threadid, numtask);
                break;
            }  
        }
        pthread_mutex_unlock(&tasklist_mutex);

        assert(task != NULL);

        //恢复task-》pathz在 thread_cnf的状态
        //pthread_mutex_lock(&path_mutex[threadid]);
            //print_vars(task->vars_set, task->n_univar);
        task_reload(thread_cnf[threadid], task, threadid);
        //pthread_mutex_unlock(&path_mutex[threadid]);
        
        //now is running normally
        pthread_mutex_lock(&stop_state_mutex);
            stop_state[threadid] = false;
        pthread_mutex_unlock(&stop_state_mutex);
        // 分支，留下一些新任务， 注意，如果分支被写进task里，本thread必须舍弃该分支赋值，不会再访问
        dpllresult* res = DPLLalgorithm2(thread_cnf[threadid], threadid);
    
        if (res->sat){
            printf("[thread %d] found an solution\n", threadid);
            //print_cnf(thread_cnf[threadid]);
            pthread_mutex_lock(&continue_mutex);
            stop = true;
            pthread_mutex_unlock(&continue_mutex);
            break;
        }
        else{
            //printf("[thread %d] in waiting state\n", threadid);
            //这个分支行不通，
            pthread_mutex_lock(&stop_state_mutex);
            stop_state[threadid] = true;
            pthread_mutex_unlock(&stop_state_mutex);
            pthread_cond_signal(&cond);
        }
    }
    return NULL;
}

void print_vars(variable* vars, int n){
    int nn = n > 10 ? 10 : n;
    for(int i = 0; i < nn; i++){
        printf("id: %d | assign %d | value %d | skip %d | sign %d\n", 
        vars[i].name, vars[i].assigned, vars[i].value, vars[i].skip, vars[i].sign);
    }
    printf("==============================\n");
}
static void set_variable_value2(cnf* cnf, variable* var, _bool value, _bool skip){
    assert(sizeof(variable) == sizeof(int));//security check
    int name = var->name;
    //timer_start(&tm);
#ifdef __serial
    for(int i = 0; i < cnf->nvar; i++){
        if(name == cnf->vars[i].name){
            cnf->vars[i].assigned = true;
            cnf->vars[i].value = value;
            cnf->vars[i].skip = skip;
            //printf("index %d, set flag to %d\n", i,  cnf->vars[i].flag);
        }
    }
    for(int i = 0; i < cnf->n_univar; i++){
        if (name == cnf->var_set[i].name){
            cnf->var_set[i].assigned = true;
            cnf->var_set[i].value = value;
            cnf->var_set[i].skip = skip;
        }
    }
#endif 
#ifdef __vector
    TODO();
#endif
}
dpllresult results[THREADNUM];
static dpllresult* branch_on_variable2(variable* var, cnf* oldcnf, int threadid);

static dpllresult* DPLLalgorithm2(cnf* cnf, int threadid){
    // check stopper
    pthread_mutex_lock(&continue_mutex);
    if (stop) {
        pthread_mutex_unlock(&continue_mutex);
        results[threadid].sat = false;
        results[threadid].model_cnf = NULL;
        return &results[threadid];
    }
    pthread_mutex_unlock(&continue_mutex);
    
    // if (threshold > 200000) {
    //     results[threadid].sat = false;
    //     results[threadid].model_cnf = NULL;

    //     pthread_mutex_lock(&continue_mutex);
    //         stop = true;
    //     pthread_mutex_unlock(&continue_mutex);
    //     return &results[threadid];
    // }

    variable* var;
    
    // Is the formula sat for the given partial model?
    if(ALL_CLAUSES_ARE_TRUE(cnf->clause_set, cnf->nclause)){
        printf("!!!!!!!!!!!!!!!!!!!!!!\n");
        results[threadid].sat = true;
        results[threadid].model_cnf = cnf;
        return &results[threadid];
    }
    //printf("[thread %d] ckpt1\n", threadid);
    // Is the formula unsatisfiable for the given partial model?
    if(ONE_CLAUSE_IS_FALSE(cnf->clause_set, cnf->nclause)){
        //printf("[thread %d]conflict happend\n", threadid);
        results[threadid].sat = false;
        results[threadid].model_cnf = cnf;
        return &results[threadid];
    }
    //printf("[thread %d] ckpt2\n", threadid);

    // Pure literal rule
    var = FIND_PURE_VAR(cnf);
    if (var != NULL){
        //printf("[thread %d]pure rule on %d, set to %d\n", threadid,var->name, var->sign);
        set_variable_value2(cnf, var, var->sign, 0);
        return DPLLalgorithm2(cnf, threadid);
    }
    //printf("[thread %d] ckpt3\n", threadid);

    // Unit clause rule
    var = FIND_UNIT_CLAUSE(cnf);
    if (var != NULL){
        set_variable_value2(cnf, var, var->sign, 0);
        //if (CERR_LEVEL >= 2){
        //printf("[thread %d]unit rule on %d\n",threadid, var->name);
        //}
        return DPLLalgorithm2(cnf, threadid);
    }

    // branch on first unassigned variable
    var = find_first_unassigned(cnf->vars, cnf->nvar);
    //printf("[thread %d] found unassigned %d var\n", threadid, var->name);
    if(var == NULL){
        results[threadid].model_cnf = NULL;
        results[threadid].sat = false;
        CERR_LEVELS[threadid] = 0;
        return &results[threadid];
    }
    else{
        return branch_on_variable2(var, cnf, threadid);
    }
}



static dpllresult* DPLLalgorithm2(cnf* cnf, int threadid);
static dpllresult* branch_on_variable2(variable* var, cnf* oldcnf, int threadid){
    threshold++;
    //printf("[thread %d]current threshold %d\n",threadid, threshold);

    //printf("[thread %d] branch on %d \n",threadid, var->name);
    _bool solve_locally = true;
    if (solve_locally){
        //if use dpll
        if (1){
            //this time we don't need copy a new cnf, 
            //we work on original cnf 
            cnf* copycnf = new_cnf_from(oldcnf);

            //we try to add a new task
            _bool skipfalse = false;
                if (numtask < THREADNUM){
                    //printf("[thread %d]try add new task\n", threadid);
                   //new assignment 2
                    set_variable_value2(copycnf, var, false, false); 
                    dpll_task_t* task = new_task(copycnf->var_set, copycnf->n_univar);
                    pthread_mutex_lock(&tasklist_mutex);
                        list_add_after(&task_list, &task->entry);  //  插入列表
                        numtask++;
                    pthread_mutex_unlock(&tasklist_mutex);
                
                    skipfalse = true;
                    //print_cnf(copycnf);
                    //printf("[thread %d]add new task to list, now there are %d tasks\n", threadid, numtask);
                    pthread_cond_signal(&cond); //send signal call others
                }else{
                    //printf("[thread %d]doesn't add ,now there are %d tasks\n", threadid, numtask);
                }

            /**
             * skip false if var=0 is set in tasks
             */
            //printf("[thread %d] try to set var:%d true t\n", threadid, var->name);

            set_variable_value2(copycnf, var, true, false);
            //if (skipfalse)print_cnf(copycnf);
            CERR_LEVELS[threadid]++;
            dpllresult* result = DPLLalgorithm2(copycnf, threadid);
            CERR_LEVELS[threadid]--;
            if (result->sat){
                /**
                 * stop everything
                 */
                pthread_mutex_lock(&continue_mutex);
                stop = true;    
                pthread_mutex_unlock(&continue_mutex);
                return result;
            }
            else{
                //job is thrown into task queue
                if (skipfalse){
                    //printf("[thread %d] skip false\n", threadid);
                    return result; 
                }   
                delete_cnf(copycnf); 
                //printf("[thread %d] try to set var:%d false\n", threadid, var->name);
                //old one is also ok
                set_variable_value2(oldcnf, var, false, false);
                //print_cnf(oldcnf);
                CERR_LEVELS[threadid]++;
                result =  DPLLalgorithm2(oldcnf, threadid);
                CERR_LEVELS[threadid]--;
                return result;
            }
        }else{
            TODO();
        }
    }
    else{
        TODO();
    }
}

static void unset_variable_value2(cnf* cnf, variable* var){
    for(int i = 0; i < cnf->nvar; i++){
        if(var->name == cnf->vars[i].name){
            cnf->vars[i].assigned = false;
        }   
    }
    for(int i = 0; i < cnf->n_univar; i++){
        if(var->name== cnf->var_set[i].name){
            cnf->var_set[i].assigned = false;
            break;
        }
    }
}
static void task_reload(cnf* cnf, dpll_task_t* task, int threadid){
    //we guaruntee that every cnf is blocked when copy, 
    //so change on single variable will go over all cnf->vars
    //which means we don't need to check all of them
    //printf("reload\n");
    //print_vars(task->vars_set, task->n_univar);
    variable* taskvarset = task->vars_set;
    int n_univar = task->n_univar;
    if(n_univar != cnf->n_univar){
        printf("inner error n_univar\n");
        exit(0);
    };

    for(int i = 0; i < n_univar; i++){
        if(taskvarset[i].name != cnf->var_set[i].name) {
            printf("inner error 2\n");
            exit(0);
        }
        if(!taskvarset[i].assigned && cnf->var_set[i].assigned){
            unset_variable_value2(cnf, &taskvarset[i]);
 
        }
        if(taskvarset[i].assigned){
            //adjust different flag
            //printf("$$$$$$$$$$$$$\n");
            set_variable_value2(cnf, &taskvarset[i], taskvarset[i].value, false);
        }
    }
    //printf("[thread %d]LOADED IN\n", threadid);
    //print_cnf(cnf);
    // if(threshold > 1)exit(0);
    //printf("task reload fine\n");
}


static void create_all_thread(cnf* _cnf){
    for(int i = 0; i < THREADNUM; i++){
        params[i].threadID = i;        
        thread_cnf[i] = new_cnf_from(_cnf);
        printf("[thread %d] cnf addr: %p\n", i, thread_cnf[i]);
        pthread_create(&thread[i], NULL, DPLLalgo_thread, (void*)&params[i]);
    }
}

static void init_task_list(cnf* cnf){
    list_init(&task_list); //初始化表格

    //建立第一条任务
    printf("first task inited\n");
    dpll_task_t* firsttask = new_task(cnf->var_set, cnf->n_univar); 

    list_add_after(&task_list, &firsttask->entry);  //  插入列表
    numtask++;
}

static dpllresult* DPLLalgorithm_pth(cnf* cnf){
    init_all_mutex();   //init所有的mutex

    init_task_list(cnf);   //init task list

    create_all_thread(cnf); 

    //
    for(int i = 0; i < THREADNUM; i++){
        pthread_join(thread[i], NULL);
    }

    for(int i = 0; i < THREADNUM; i++){
        if (results[i].sat)
            return &results[i];
    }
    return &results[0];
}